@inproceedings{Sommer:2014er,
 author = {Sommer, Robin and Vallentin, Matthias and De Carli, Lorenzo and Paxson, Vern},
 title = {HILTI: An Abstract Execution Environment for Deep, Stateful Network Traffic Analysis},
 booktitle = {Proceedings of the 2014 Conference on Internet Measurement Conference},
 series = {IMC '14},
 year = {2014},
 isbn = {978-1-4503-3213-2},
 location = {Vancouver, BC, Canada},
 pages = {461--474},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2663716.2663735},
 doi = {10.1145/2663716.2663735},
 acmid = {2663735},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {deep packet inspection, intrusion detection, real-time monitoring},
} 

@article{Shiravi:2012hr,
  title={Toward Developing a Dystematic Approach to Generate Benchmark Datasets for Intrusion Tetection},
  author={Shiravi, Ali and Shiravi, Hadi and Tavallaee, Mahbod and Ghorbani, Ali A},
  journal={Computers \& Security},
  volume={31},
  number={3},
  pages={357--374},
  year={2012},
  publisher={Elsevier}
}

@inproceedings{DeCarli:2014:BPM:2660267.2660361,
 author = {De Carli, Lorenzo and Sommer, Robin and Jha, Somesh},
 title = {Beyond Pattern Matching: A Concurrency Model for Stateful Deep Packet Inspection},
 booktitle = {Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security},
 series = {CCS '14},
 year = {2014},
 isbn = {978-1-4503-2957-6},
 location = {Scottsdale, Arizona, USA},
 pages = {1378--1390},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2660267.2660361},
 doi = {10.1145/2660267.2660361},
 acmid = {2660361},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {flexible intrusion detection, nids, scalable traffic analysis},
} 

@inproceedings{vallentin2016vast,
author = {Matthias Vallentin and Vern Paxson and Robin Sommer},
title = {VAST: A Unified Platform for Interactive Network Forensics},
booktitle = {13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16)},
year = {2016},
month = Mar,
isbn = {978-1-931971-29-4},
address = {Santa Clara, CA},
pages = {345--362},
url = {https://www.usenix.org/conference/nsdi16/technical-sessions/presentation/vallentin},
publisher = {USENIX Association},
}	

@article{liao2013intrusion,
  title={Intrusion Detection System: A Comprehensive Review},
  author={Liao, Hung-Jen and Lin, Chun-Hung Richard and Lin, Ying-Chih and Tung, Kuang-Yuan},
  journal={Journal of Network and Computer Applications},
  volume={36},
  number={1},
  pages={16--24},
  year={2013},
  publisher={Elsevier}
}

@inproceedings{Ning:2003:LAS:948109.948137,
 author = {Ning, Peng and Xu, Dingbang},
 title = {Learning Attack Strategies from Intrusion Alerts},
 booktitle = {Proceedings of the 10th ACM Conference on Computer and Communications Security},
 series = {CCS '03},
 year = {2003},
 isbn = {1-58113-738-9},
 location = {Washington D.C., USA},
 pages = {200--209},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/948109.948137},
 doi = {10.1145/948109.948137},
 acmid = {948137},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {alert correlation, intrusion detection, profiling attack strategies},
} 

@inproceedings{1004372, 
author={F. Cuppens and A. Miege}, 
booktitle={Proceedings 2002 IEEE Symposium on Security and Privacy}, 
title={Alert Correlation in a Cooperative Intrusion Detection Framework}, 
year={2002}, 
pages={202-215}, 
keywords={authorisation;CRIM;MIRADOR project;alert clustering;alert correlation;alert management;alert merging;cooperative intrusion detection framework;global alerts;synthetic alerts;Collaboration;Data security;Dissolved gas analysis;Information security;Intrusion detection;Laboratories;Merging;Pattern matching}, 
doi={10.1109/SECPRI.2002.1004372}, 
ISSN={1081-6011}, 
month={},}

@inproceedings{viswanathan2011semantic,
  title={A Semantic Framework for Data Analysis in Networked Systems},
  author={Viswanathan, Arun and Hussain, Alefiya and Mirkovic, Jelena and Schwab, Stephen and Wroclawski, John},
  booktitle={Proceedings of NSDI’11: 8th USENIX Symposium on Networked Systems Design and Implementation},
  pages={127},
  year={2011},
  organization={Citeseer}
}
@article{Lamport:1994:TLA:177492.177726,
 author = {Lamport, Leslie},
 title = {The Temporal Logic of Actions},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {May 1994},
 volume = {16},
 number = {3},
 month = may,
 year = {1994},
 issn = {0164-0925},
 pages = {872--923},
 numpages = {52},
 url = {http://doi.acm.org/10.1145/177492.177726},
 doi = {10.1145/177492.177726},
 acmid = {177726},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrent programming, liveness properties, safety properties},
} 
@article{Allen:1983:MKT:182.358434,
 author = {Allen, James F.},
 title = {Maintaining Knowledge About Temporal Intervals},
 journal = {Commun. ACM},
 issue_date = {Nov. 1983},
 volume = {26},
 number = {11},
 month = nov,
 year = {1983},
 issn = {0001-0782},
 pages = {832--843},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/182.358434},
 doi = {10.1145/182.358434},
 acmid = {358434},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {interval reasoning, interval representation, temporal interval},
} 
@inproceedings{Hewitt:1973:UMA:1624775.1624804,
 author = {Hewitt, Carl and Bishop, Peter and Steiger, Richard},
 title = {A Universal Modular ACTOR Formalism for Artificial Intelligence},
 booktitle = {Proceedings of the 3rd International Joint Conference on Artificial Intelligence},
 series = {IJCAI'73},
 year = {1973},
 location = {Stanford, USA},
 pages = {235--245},
 numpages = {11},
 url = {http://dl.acm.org/citation.cfm?id=1624775.1624804},
 acmid = {1624804},
 publisher = {Morgan Kaufmann Publishers Inc.},
 address = {San Francisco, CA, USA},
} 
@incollection{hoare1978communicating,
  title={Communicating sequential processes},
  author={Hoare, Charles Antony Richard},
  booktitle={The origin of concurrent programming},
  pages={413--443},
  year={1978},
  publisher={Springer}
}
@inproceedings {raft:2014,
author = {Diego Ongaro and John Ousterhout},
title = {In Search of an Understandable Consensus Algorithm},
booktitle = {2014 USENIX Annual Technical Conference (USENIX ATC 14)},
year = {2014},
month = Jun,
isbn = {978-1-931971-10-2},
address = {Philadelphia, PA},
pages = {305--319},
url = {https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro},
publisher = {USENIX Association},
}

@article{lirui2015,
  title={一种密闭可重构网络安全测试床的设计与实现},
  author={李睿 and 朱俊虎 and 王清贤 and 周天阳 },
  journal={信息工程大学学报},
  volume={16},
  number={1},
  pages={111--116},
  year={2015}
}
@inproceedings{Roger:2001:LAT:872752.873518,
 author = {Roger, Muriel and Goubault-Larrecq, Jean},
 title = {Log Auditing Through Model-Checking},
 booktitle = {Proceedings of the 14th IEEE Workshop on Computer Security Foundations},
 series = {CSFW '01},
 year = {2001},
 pages = {220--},
 url = {http://dl.acm.org/citation.cfm?id=872752.873518},
 acmid = {873518},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
} 
@inproceedings{Ellis:2004:BAW:1029618.1029625,
 author = {Ellis, Daniel R. and Aiken, John G. and Attwood, Kira S. and Tenaglia, Scott D.},
 title = {A Behavioral Approach to Worm Detection},
 booktitle = {Proceedings of the 2004 ACM Workshop on Rapid Malcode},
 series = {WORM '04},
 year = {2004},
 isbn = {1-58113-970-5},
 location = {Washington DC, USA},
 pages = {43--53},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1029618.1029625},
 doi = {10.1145/1029618.1029625},
 acmid = {1029625},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {behavioral signatures, descendant relation, intrusion detection, network application architecture, network worms},
} 
@inproceedings{Kinder05detectingmalicious,
    author = {Johannes Kinder and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith and Technische Universität München},
    title = {Detecting malicious code by model checking},
    booktitle = {Proceedings of the 2nd International Conference on Intrusion and Malware Detection and Vulnerability Assessment (DIMVA’05), volume 3548 of Lecture Notes in Computer Science},
    year = {2005},
    pages = {174--187},
    publisher = {Springer Berlin}
}
@Inbook{Naldurg2004,
author={Naldurg, Prasad
and Sen, Koushik
and Thati, Prasanna},
editor={de Frutos-Escrig, David and N{\'u}{\~{n}}ez, Manuel},
title={A Temporal Logic Based Framework for Intrusion Detection},
bookTitle={Formal Techniques for Networked and Distributed Systems -- FORTE 2004: 24th IFIP WG 6.1 International Conference, Madrid Spain, September 27-30, 2004. Proceedings},
year={2004},
publisher={Springer Berlin Heidelberg},
address={Berlin, Heidelberg},
pages={359--376},
isbn={978-3-540-30232-2},
doi={10.1007/978-3-540-30232-2_23},
url={http://dx.doi.org/10.1007/978-3-540-30232-2_23}
}
@article{Basin:2013:MDU:2554420.2554425,
 author = {Basin, David and Harvan, Matus and Klaedtke, Felix and Z\v{a}linescu, Eugen},
 title = {Monitoring Data Usage in Distributed Systems},
 journal = {IEEE Trans. Softw. Eng.},
 issue_date = {October 2013},
 volume = {39},
 number = {10},
 month = oct,
 year = {2013},
 issn = {0098-5589},
 pages = {1403--1426},
 numpages = {24},
 url = {http://dx.doi.org/10.1109/TSE.2013.18},
 doi = {10.1109/TSE.2013.18},
 acmid = {2554425},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 keywords = {regulation,Monitors,temporal logic,verification,distributed systems},
}
@article{Marchetti2016127,
title = "Analysis of high volumes of network traffic for Advanced Persistent Threat detection ",
journal = "Computer Networks ",
volume = "109, Part 2",
number = "",
pages = "127 - 141",
year = "2016",
note = "Traffic and Performance in the Big Data Era ",
issn = "1389-1286",
doi = "http://dx.doi.org/10.1016/j.comnet.2016.05.018",
url = "http://www.sciencedirect.com/science/article/pii/S1389128616301633",
author = "Mirco Marchetti and Fabio Pierazzi and Michele Colajanni and Alessandro Guido",
keywords = "Security analytics",
keywords = "Traffic analysis",
keywords = "Advanced Persistent Threats",
keywords = "Data exfiltration "
}
@inproceedings{Bersani:2016:ELT:2884781.2884832,
 author = {Bersani, Marcello M. and Bianculli, Domenico and Ghezzi, Carlo and Krsti\'{c}, Sr\&\#273;an and Pietro, Pierluigi San},
 title = {Efficient Large-scale Trace Checking Using Mapreduce},
 booktitle = {Proceedings of the 38th International Conference on Software Engineering},
 series = {ICSE '16},
 year = {2016},
 isbn = {978-1-4503-3900-1},
 location = {Austin, Texas},
 pages = {888--898},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/2884781.2884832},
 doi = {10.1145/2884781.2884832},
 acmid = {2884832},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@article{Basin:2015:MMF:2772377.2699444,
 author = {Basin, David and Klaedtke, Felix and M\"{u}ller, Samuel and Z\u{a}linescu, Eugen},
 title = {Monitoring Metric First-Order Temporal Properties},
 journal = {J. ACM},
 issue_date = {May 2015},
 volume = {62},
 number = {2},
 month = may,
 year = {2015},
 issn = {0004-5411},
 pages = {15:1--15:45},
 articleno = {15},
 numpages = {45},
 url = {http://doi.acm.org/10.1145/2699444},
 doi = {10.1145/2699444},
 acmid = {2699444},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Runtime verification, automatic structures, compliance checking, security policies, temporal databases},
} 
@INPROCEEDINGS{johnson2013, 
author={J. R. Johnson and E. A. Hogan}, 
booktitle={2013 IEEE International Conference on Intelligence and Security Informatics}, 
title={A graph analytic metric for mitigating advanced persistent threat}, 
year={2013}, 
pages={129-133}, 
keywords={authorisation;computer network security;graph theory;advanced persistent threat mitigation;auditing layers;authorization layers;cyber network vulnerability;edge selection;edge vertices;graph analytic metrics;lateral movement;network security authorization phase;node selection;oriented subgraph;predictive deterrence;privilege escalation;Authentication;Authorization;Graph theory;Heuristic algorithms;Measurement;Presses;cybersecurity;discrete mathematics;graph theory}, 
doi={10.1109/ISI.2013.6578801}, 
month={June},}
@article{Friedberg201535,
title = {Combating advanced persistent threats: From network event correlation to incident detection},
journal = {Computers \& Security},
volume = "48",
number = "",
pages = "35 - 57",
year = "2015",
note = "",
issn = "0167-4048",
doi = "http://dx.doi.org/10.1016/j.cose.2014.09.006",
url = "http://www.sciencedirect.com/science/article/pii/S0167404814001461",
author = "Ivo Friedberg and Florian Skopik and Giuseppe Settanni and Roman Fiedler",
keywords = "Advanced persistent threat",
keywords = "Anomaly detection",
keywords = "Log file analysis",
keywords = "Intrusion detection",
keywords = "Event correlation",
keywords = "Self-learning system model "
}
@article{Shiravi2012357,
title = "Toward developing a systematic approach to generate benchmark datasets for intrusion detection ",
journal = {Computers \& Security},
volume = "31",
number = "3",
pages = "357 - 374",
year = "2012",
note = "",
issn = "0167-4048",
doi = "http://dx.doi.org/10.1016/j.cose.2011.12.012",
url = "http://www.sciencedirect.com/science/article/pii/S0167404811001672",
author = "Ali Shiravi and Hadi Shiravi and Mahbod Tavallaee and Ali A. Ghorbani",
keywords = "Intrusion detection",
keywords = "Dataset generation",
keywords = "Network traffic profile "
}
@article{García2014100,
title = "An empirical comparison of botnet detection methods ",
journal = {Computers \& Security },
volume = "45",
number = "",
pages = "100 - 123",
year = "2014",
note = "",
issn = "0167-4048",
doi = "http://dx.doi.org/10.1016/j.cose.2014.05.011",
url = "http://www.sciencedirect.com/science/article/pii/S0167404814000923",
author = "S. García and M. Grill and J. Stiborek and A. Zunino",
keywords = "Botnet detection",
keywords = "Malware detection",
keywords = "Methods comparison",
keywords = "Botnet dataset",
keywords = "Anomaly detection",
keywords = "Network traffic "
}
@ARTICLE{igure2008, 
author={V. M. Igure and R. D. Williams}, 
journal={IEEE Communications Surveys Tutorials}, 
title={Taxonomies of attacks and vulnerabilities in computer systems}, 
year={2008}, 
volume={10}, 
number={1}, 
pages={6-19}, 
keywords={telecommunication security;computer system attacks;computer system vulnerabilities;information organization;security assessment;taxonomies;Buildings;Communication system security;Data security;Databases;Information security;Organizing;Standards publication;Taxonomy}, 
doi={10.1109/COMST.2008.4483667}, 
ISSN={1553-877X}, 
month={First},}
@article{Meng:2015:CSS:2808687.2785733,
 author = {Meng, Guozhu and Liu, Yang and Zhang, Jie and Pokluda, Alexander and Boutaba, Raouf},
 title = {Collaborative Security: A Survey and Taxonomy},
 journal = {ACM Comput. Surv.},
 issue_date = {September 2015},
 volume = {48},
 number = {1},
 month = jul,
 year = {2015},
 issn = {0360-0300},
 pages = {1:1--1:42},
 articleno = {1},
 numpages = {42},
 url = {http://doi.acm.org/10.1145/2785733},
 doi = {10.1145/2785733},
 acmid = {2785733},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Collaborative security, information sharing, intrusion detection, malware, privacy, spam, taxonomy, trust},
} 
@article{Ahmed:2016:SNA:2894395.2894710,
 author = {Ahmed, Mohiuddin and Naser Mahmood, Abdun and Hu, Jiankun},
 title = {A Survey of Network Anomaly Detection Techniques},
 journal = {J. Netw. Comput. Appl.},
 issue_date = {January 2016},
 volume = {60},
 number = {C},
 month = jan,
 year = {2016},
 issn = {1084-8045},
 pages = {19--31},
 numpages = {13},
 url = {http://dx.doi.org/10.1016/j.jnca.2015.11.016},
 doi = {10.1016/j.jnca.2015.11.016},
 acmid = {2894710},
 publisher = {Academic Press Ltd.},
 address = {London, UK, UK},
 keywords = {Anomaly detection, Classification, Clustering, Computer security, Information theory, Intrusion detection},
} 
@article{Liao:2013:RID:2405859.2406209,
 author = {Liao, Hung-Jen and Richard Lin, Chun-Hung and Lin, Ying-Chih and Tung, Kuang-Yuan},
 title = {Review: Intrusion Detection System: A Comprehensive Review},
 journal = {J. Netw. Comput. Appl.},
 issue_date = {January, 2013},
 volume = {36},
 number = {1},
 month = jan,
 year = {2013},
 issn = {1084-8045},
 pages = {16--24},
 numpages = {9},
 url = {http://dx.doi.org/10.1016/j.jnca.2012.09.004},
 doi = {10.1016/j.jnca.2012.09.004},
 acmid = {2406209},
 publisher = {Academic Press Ltd.},
 address = {London, UK, UK},
 keywords = {Anomaly, Intrusion detection, Misuse},
} 
@article{Khan2016,
	author = {Khan, Suleman and Gani, Abdullah and Wahab, Ainuddin Wahid Abdul and Shiraz, Muhammad and Ahmad, Iftikhar},
	doi = {10.1016/j.jnca.2016.03.005},
	journal = {Journal of Network and Computer Applications},
	keywords = {Forensic; Investigation; Cybercrimes; Digital evidence; Intrusion detection},
	language = {English},
	number = {Complete},
	pages = {214-235},
	title = {Review},
	volume = {66},
	year = {2016},
}
@article{Dillon:1994:GIL:192218.192226,
 author = {Dillon, L. K. and Kutty, G. and Moser, L. E. and Melliar-Smith, P. M. and Ramakrishna, Y. S.},
 title = {A Graphical Interval Logic for Specifying Concurrent Systems},
 journal = {ACM Trans. Softw. Eng. Methodol.},
 issue_date = {April 1994},
 volume = {3},
 number = {2},
 month = apr,
 year = {1994},
 issn = {1049-331X},
 pages = {131--165},
 numpages = {35},
 url = {http://doi.acm.org/10.1145/192218.192226},
 doi = {10.1145/192218.192226},
 acmid = {192226},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {automated proof-checking, concurrent systems, formal specifications, graphical interval logic, temporal logic, timing diagrams, visual languages},
} 
@inproceedings{Barringer:1984:YMC:800057.808665,
 author = {Barringer, Howard and Kuiper, Ruurd and Pnueli, Amir},
 title = {Now You May Compose Temporal Logic Specifications},
 booktitle = {Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing},
 series = {STOC '84},
 year = {1984},
 isbn = {0-89791-133-4},
 pages = {51--63},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/800057.808665},
 doi = {10.1145/800057.808665},
 acmid = {808665},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@article{Lamport:1994:TLA:177492.177726,
 author = {Lamport, Leslie},
 title = {The Temporal Logic of Actions},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {May 1994},
 volume = {16},
 number = {3},
 month = may,
 year = {1994},
 issn = {0164-0925},
 pages = {872--923},
 numpages = {52},
 url = {http://doi.acm.org/10.1145/177492.177726},
 doi = {10.1145/177492.177726},
 acmid = {177726},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrent programming, liveness properties, safety properties},
} 
@Inbook{Wolper1989,
author="Wolper, Pierre",
editor="Banieqbal, B.
and Barringer, H.
and Pnueli, A.",
title="On the relation of programs and computations to models of temporal logic",
bookTitle="Temporal Logic in Specification: Altrincham, UK, April 8--10, 1987 Proceedings",
year="1989",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="75--123",
isbn="978-3-540-46811-0",
doi="10.1007/3-540-51803-7_23",
url="http://dx.doi.org/10.1007/3-540-51803-7_23"
}
@Inbook{Kinder2005,
author="Kinder, Johannes
and Katzenbeisser, Stefan
and Schallhart, Christian
and Veith, Helmut",
editor="Julisch, Klaus
and Kruegel, Christopher",
title="Detecting Malicious Code by Model Checking",
bookTitle="Detection of Intrusions and Malware, and Vulnerability Assessment: Second International Conference, DIMVA 2005, Vienna, Austria, July 7-8, 2005. Proceedings",
year="2005",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="174--187",
isbn="978-3-540-31645-9",
doi="10.1007/11506881_11",
url="http://dx.doi.org/10.1007/11506881_11"
}
@inproceedings{Hussain:2003:FCD:863955.863968,
 author = {Hussain, Alefiya and Heidemann, John and Papadopoulos, Christos},
 title = {A Framework for Classifying Denial of Service Attacks},
 booktitle = {Proceedings of the 2003 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications},
 series = {SIGCOMM '03},
 year = {2003},
 isbn = {1-58113-735-4},
 location = {Karlsruhe, Germany},
 pages = {99--110},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/863955.863968},
 doi = {10.1145/863955.863968},
 acmid = {863968},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {denial of service attacks, measurement, security, time series analysis},
} 
@inproceedings{Ellis:2004:BAW:1029618.1029625,
 author = {Ellis, Daniel R. and Aiken, John G. and Attwood, Kira S. and Tenaglia, Scott D.},
 title = {A Behavioral Approach to Worm Detection},
 booktitle = {Proceedings of the 2004 ACM Workshop on Rapid Malcode},
 series = {WORM '04},
 year = {2004},
 isbn = {1-58113-970-5},
 location = {Washington DC, USA},
 pages = {43--53},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1029618.1029625},
 doi = {10.1145/1029618.1029625},
 acmid = {1029625},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {behavioral signatures, descendant relation, intrusion detection, network application architecture, network worms},
} 
@inproceedings{Basin:2010:MSP:1809842.1809849,
 author = {Basin, David and Klaedtke, Felix and M\"{u}ller, Samuel},
 title = {Monitoring Security Policies with Metric First-order Temporal Logic},
 booktitle = {Proceedings of the 15th ACM Symposium on Access Control Models and Technologies},
 series = {SACMAT '10},
 year = {2010},
 isbn = {978-1-4503-0049-0},
 location = {Pittsburgh, Pennsylvania, USA},
 pages = {23--34},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1809842.1809849},
 doi = {10.1145/1809842.1809849},
 acmid = {1809849},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {access control, compliance, monitoring, security policies, separation of duty, temporal logic, usage control},
} 
@inproceedings{Zaharia:2012:RDD:2228298.2228301,
 author = {Zaharia, Matei and Chowdhury, Mosharaf and Das, Tathagata and Dave, Ankur and Ma, Justin and McCauley, Murphy and Franklin, Michael J. and Shenker, Scott and Stoica, Ion},
 title = {Resilient Distributed Datasets: A Fault-tolerant Abstraction for In-memory Cluster Computing},
 booktitle = {Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation},
 series = {NSDI'12},
 year = {2012},
 location = {San Jose, CA},
 pages = {2--2},
 numpages = {1},
 url = {http://dl.acm.org/citation.cfm?id=2228298.2228301},
 acmid = {2228301},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 
@INPROCEEDINGS{4567924, 
author={A. Pnueli}, 
booktitle={18th Annual Symposium on Foundations of Computer Science (sfcs 1977)}, 
title={The temporal logic of programs}, 
year={1977}, 
pages={46-57}, 
keywords={Clocks;Logic;Operating systems;Power system modeling;Programming profession;Real time systems;Reasoning about programs;Safety;Stress;System recovery}, 
doi={10.1109/SFCS.1977.32}, 
ISSN={0272-5428}, 
month={Oct},}
@Inbook{Ouaknine2008,
author="Ouaknine, Jo{\"e}l
and Worrell, James",
editor="Cassez, Franck
and Jard, Claude",
title="Some Recent Results in Metric Temporal Logic",
bookTitle="Formal Modeling and Analysis of Timed Systems: 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="1--13",
isbn="978-3-540-85778-5",
doi="10.1007/978-3-540-85778-5_1",
url="http://dx.doi.org/10.1007/978-3-540-85778-5_1"
}
@article{Alur:1994:RTL:174644.174651,
 author = {Alur, Rajeev and Henzinger, Thomas A.},
 title = {A Really Temporal Logic},
 journal = {J. ACM},
 issue_date = {Jan. 1994},
 volume = {41},
 number = {1},
 month = jan,
 year = {1994},
 issn = {0004-5411},
 pages = {181--203},
 numpages = {23},
 url = {http://doi.acm.org/10.1145/174644.174651},
 doi = {10.1145/174644.174651},
 acmid = {174651},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {EXPSPACE-completeness, dense time, discrete time, linear-time temporal logic, model checking, real-time requirements},
} 
@article{ALUR199335,
title = "Real-Time Logics: Complexity and Expressiveness",
journal = "Information and Computation",
volume = "104",
number = "1",
pages = "35 - 77",
year = "1993",
note = "",
issn = "0890-5401",
doi = "http://dx.doi.org/10.1006/inco.1993.1025",
url = "http://www.sciencedirect.com/science/article/pii/S0890540183710254",
author = "R. Alur and T.A. Henzinger",
}
@article{Alur:1996:BRP:227595.227602,
 author = {Alur, Rajeev and Feder, Tom\'{a}s and Henzinger, Thomas A.},
 title = {The Benefits of Relaxing Punctuality},
 journal = {J. ACM},
 issue_date = {Jan. 1996},
 volume = {43},
 number = {1},
 month = jan,
 year = {1996},
 issn = {0004-5411},
 pages = {116--146},
 numpages = {31},
 url = {http://doi.acm.org/10.1145/227595.227602},
 doi = {10.1145/227595.227602},
 acmid = {227602},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {model checking, real time, temporal logic, timed automata},
} 
@Inbook{Bouyer2008,
author="Bouyer, Patricia
and Markey, Nicolas
and Ouaknine, Jo{\"e}l
and Worrell, James",
editor="Aceto, Luca
and Damg{\aa}rd, Ivan
and Goldberg, Leslie Ann
and Halld{\'o}rsson, Magn{\'u}s M.
and Ing{\'o}lfsd{\'o}ttir, Anna
and Walukiewicz, Igor",
title="On Expressiveness and Complexity in Real-Time Model Checking",
bookTitle="Automata, Languages and Programming: 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="124--135",
isbn="978-3-540-70583-3",
doi="10.1007/978-3-540-70583-3_11",
url="http://dx.doi.org/10.1007/978-3-540-70583-3_11"
}
@Inbook{Ouaknine2006,
author="Ouaknine, Jo{\"e}l
and Worrell, James",
editor="Hermanns, Holger
and Palsberg, Jens",
title="Safety Metric Temporal Logic Is Fully Decidable",
bookTitle="Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006. Proceedings",
year="2006",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="411--425",
isbn="978-3-540-33057-8",
doi="10.1007/11691372_27",
url="http://dx.doi.org/10.1007/11691372_27"
}
@Inbook{Clarke1982,
author="Clarke, Edmund M.
and Emerson, E. Allen",
editor="Kozen, Dexter",
title="Design and synthesis of synchronization skeletons using branching time temporal logic",
bookTitle="Logics of Programs: Workshop, Yorktown Heights, New York, May 1981",
year="1982",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="52--71",
isbn="978-3-540-39047-3",
doi="10.1007/BFb0025774",
url="http://dx.doi.org/10.1007/BFb0025774"
}
@Article{Koymans1990,
author="Koymans, Ron",
title="Specifying real-time properties with metric temporal logic",
journal="Real-Time Systems",
year="1990",
volume="2",
number="4",
pages="255--299",
abstract="This paper is motivated by the need for a formal specification method for real-time systems. In these systemsquantitative temporal properties play a dominant role. We first characterize real-time systems by giving a classification of such quantitative temporal properties. Next, we extend the usual models for temporal logic by including a distance function to measure time and analyze what restrictions should be imposed on such a function. Then we introduce appropriate temporal operators to reason about such models by turning qualitative temporal operators into (quantitative) metric temporal operators and show how the usual quantitative temporal properties of real-time systems can be expressed in this metric temporal logic. After we illustrate the application of metric temporal logic to real-time systems by several examples, we end this paper with some conclusions.",
issn="1573-1383",
doi="10.1007/BF01995674",
url="http://dx.doi.org/10.1007/BF01995674"
}
@Inbook{Henzinger1998,
author="Henzinger, Thomas A.",
editor="Sangiorgi, Davide
and de Simone, Robert",
title="It's about time: Real-time logics reviewed",
bookTitle="CONCUR'98 Concurrency Theory: 9th International Conference Nice, France, September 8--11, 1998 Proceedings",
year="1998",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="439--454",
isbn="978-3-540-68455-8",
doi="10.1007/BFb0055640",
url="http://dx.doi.org/10.1007/BFb0055640"
}
@Inbook{Pandya2011,
author="Pandya, Paritosh K.
and Shah, Simoni S.",
editor="Katoen, Joost-Pieter
and K{\"o}nig, Barbara",
title="On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing",
bookTitle="CONCUR 2011 -- Concurrency Theory: 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings",
year="2011",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="60--75",
isbn="978-3-642-23217-6",
doi="10.1007/978-3-642-23217-6_5",
url="http://dx.doi.org/10.1007/978-3-642-23217-6_5"
}
@article{Fuyu2015,
author = {付  钰，李洪成，吴晓平，王甲生},
title = {基于大数据分析的APT攻击检测研究综述},
publisher = {通信学报},
year = {2015},
journal = {通信学报},
volume = {36},
number = {11},
eid = {1},
numpages = {13},
pages = {1},
keywords = {网络安全检测；高级持续性威胁；大数据分析；智能反馈；关联分析},
url = {http://www.infocomm-journal.com/txxb/CN/abstract/article_156465.shtml},
doi = {10.11959/j.issn.1000-436x.2015184}
}    
@ARTICLE{7307098, 
author={A. L. Buczak and E. Guven}, 
journal={IEEE Communications Surveys Tutorials}, 
title={A Survey of Data Mining and Machine Learning Methods for Cyber Security Intrusion Detection}, 
year={2016}, 
volume={18}, 
number={2}, 
pages={1153-1176}, 
keywords={computer network security;data mining;learning (artificial intelligence);DM methods;ML-DM algorithms;ML-DM method;cyber analytics;cyber data sets;cyber security intrusion detection;data mining;machine learning methods;Computer security;Data mining;Data models;IP networks;Measurement;Ports (Computers);Protocols;Cyber Analytics;Cyber analytics;Data Mining;Machine Learning;data mining;machine learning}, 
doi={10.1109/COMST.2015.2494502}, 
ISSN={1553-877X}, 
month={Secondquarter},}
@ARTICLE{6489876, 
author={S. T. Zargar and J. Joshi and D. Tipper}, 
journal={IEEE Communications Surveys Tutorials}, 
title={A Survey of Defense Mechanisms Against Distributed Denial of Service (DDoS) Flooding Attacks}, 
year={2013}, 
volume={15}, 
number={4}, 
pages={2046-2069}, 
keywords={computer network security;DDoS flooding attack problem;collaborative defense approach;comprehensive defense mechanism;comprehensive distributed defense approach;coordinated large-scale attack;distributed denial of service flooding attacks;intrusion detection;prevention research community;Denial of service;Intrusion detection;Network service;Distributed Denial of Service (DDoS) flooding attack;collaborative DDoS defense;distributed DDoS defense;intrusion detection systems;intrusion prevention systems}, 
doi={10.1109/SURV.2013.031413.00127}, 
ISSN={1553-877X}, 
month={Fourth},}
@article{Kripke1963-KRISAO,
  title = {Semantical Analysis of Modal Logic I. Normal Propositional Calculi},
  pages = {67--96},
  author = {Saul A. Kripke},
  volume = {9},
  publisher = {Wiley-Blackwell},
  number = {56},
  year = {1963},
  journal = {Zeitschrift fur mathematische Logik und Grundlagen der Mathematik}
}
@book{Prior1957,
  publisher = {Oxford University Press},
  author = {A. N. Prior},
  year = {1957},
  title = {Time and Modality},
  address = {Oxford},
}
@phdthesis{Kamp1968-KAMTLA-2,
  publisher = {Dissertation},
  school = {University of California, Los Angeles},
  author = {Johan Anthony Wilem Kamp},
  year = {1968},
  title = {Tense Logic and the Theory of Linear Order}
}
@article{Burgess1982-JOHAFT-2,
  journal = {Notre Dame Journal of Formal Logic},
  pages = {367--374},
  year = {1982},
  number = {4},
  title = {Axioms for Tense Logic. I. ``Since'' and ``Until''},
  author = {John P. Burgess},
  publisher = {Duke University Press},
  volume = {23}
}
@book{Kroger1987-KRGTLO,
  title = {Temporal Logic of Programs},
  year = {1987},
  author = {Fred Kr\"oger and European Association for Theoretical Computer Science}
}
@Inbook{Henzinger1998,
author="Henzinger, T. A.
and Raskin, J.-F.
and Schobbens, P.-Y.",
editor="Larsen, Kim G.
and Skyum, Sven
and Winskel, Glynn",
title="The regular real-time languages",
bookTitle="Automata, Languages and Programming: 25th International Colloquium, ICALP'98 Aalborg, Denmark, July 13--17, 1998 Proceedings",
year="1998",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="580--591",
isbn="978-3-540-68681-1",
doi="10.1007/BFb0055086",
url="http://dx.doi.org/10.1007/BFb0055086"
}
@INPROCEEDINGS{4276556, 
author={P. Bouyer and N. Markey and J. Ouaknine and J. Worrell}, 
booktitle={22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)}, 
title={The Cost of Punctuality}, 
year={2007}, 
pages={109-120}, 
keywords={computability;finite state machines;formal verification;temporal logic;timing;finite-state automata;linear-time temporal logic;model checking;punctual specifications;punctual timing constraints;punctuality cost;real-time logic metric temporal logic;satisfiability;Automata;Automatic logic units;Computer science;Costs;Real time systems;Time factors;Timing;Turing machines}, 
doi={10.1109/LICS.2007.49}, 
ISSN={1043-6871}, 
month={July},}
@article{Hirshfeld:2004:LRT:2370629.2370631,
 author = {Hirshfeld, Yoram and Rabinovich, Alexander},
 title = {Logics for Real Time: Decidability and Complexity},
 journal = {Fundam. Inf.},
 issue_date = {January 2004},
 volume = {62},
 number = {1},
 month = jan,
 year = {2004},
 issn = {0169-2968},
 pages = {1--28},
 numpages = {28},
 url = {http://dl.acm.org/citation.cfm?id=2370629.2370631},
 acmid = {2370631},
 publisher = {IOS Press},
 address = {Amsterdam, The Netherlands, The Netherlands},
} 
@INPROCEEDINGS{4567924, 
author={A. Pnueli}, 
booktitle={18th Annual Symposium on Foundations of Computer Science (sfcs 1977)}, 
title={The temporal logic of programs}, 
year={1977}, 
pages={46-57}, 
keywords={Clocks;Logic;Operating systems;Power system modeling;Programming profession;Real time systems;Reasoning about programs;Safety;Stress;System recovery}, 
doi={10.1109/SFCS.1977.32}, 
ISSN={0272-5428}, 
month={Oct},}
@book{Berard:2010:SSV:1965314,
 author = {Berard, B. and Bidoit, M. and Finkel, A. and Laroussinie, F. and Petit, A. and Petrucci, L. and Schnoebelen, P.},
 title = {Systems and Software Verification: Model-Checking Techniques and Tools},
 year = {2010},
 isbn = {3642074782, 9783642074783},
 edition = {1st},
 publisher = {Springer Publishing Company, Incorporated},
} 
@article{EMERSON19851,
title = "Decision procedures and expressiveness in the temporal logic of branching time",
journal = "Journal of Computer and System Sciences",
volume = "30",
number = "1",
pages = "1 - 24",
year = "1985",
note = "",
issn = "0022-0000",
doi = "http://dx.doi.org/10.1016/0022-0000(85)90001-7",
url = "http://www.sciencedirect.com/science/article/pii/0022000085900017",
author = "E.Allen Emerson and Joseph Y. Halpern",
}
@article{ALLENEMERSON1987275,
title = "Modalities for model checking: branching time logic strikes back",
journal = "Science of Computer Programming",
volume = "8",
number = "3",
pages = "275 - 306",
year = "1987",
note = "",
issn = "0167-6423",
doi = "http://dx.doi.org/10.1016/0167-6423(87)90036-0",
url = "http://www.sciencedirect.com/science/article/pii/0167642387900360",
author = "E. Allen Emerson and Chin-Laung Lei",
}
@article{Emerson:1986:LLN:4904.4999,
 author = {Emerson, E. Allen and Halpern, Joseph Y.},
 title = {\&Ldquo;Sometimes\&Rdquo; and \&Ldquo;Not Never\&Rdquo; Revisited: On Branching Versus Linear Time Temporal Logic},
 journal = {J. ACM},
 issue_date = {Jan. 1986},
 volume = {33},
 number = {1},
 month = jan,
 year = {1986},
 issn = {0004-5411},
 pages = {151--178},
 numpages = {28},
 url = {http://doi.acm.org/10.1145/4904.4999},
 doi = {10.1145/4904.4999},
 acmid = {4999},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@inproceedings{Schwartz:1983:ILH:800221.806720,
 author = {Schwartz, Richard L. and Melliar-Smith, P. M. and Vogt, Friedrich H.},
 title = {An Interval Logic for Higher-level Temporal Reasoning},
 booktitle = {Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing},
 series = {PODC '83},
 year = {1983},
 isbn = {0-89791-110-5},
 location = {Montreal, Quebec, Canada},
 pages = {173--186},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/800221.806720},
 doi = {10.1145/800221.806720},
 acmid = {806720},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@Inbook{Moszkowski1984,
author="Moszkowski, Ben
and Manna, Zohar",
editor="Clarke, Edmund
and Kozen, Dexter",
title="Reasoning in interval temporal logic",
bookTitle="Logics of Programs: Workshop, Carnegie Mellon University Pittsburgh, PA, June 6--8, 1983",
year="1984",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="371--382",
isbn="978-3-540-38775-6",
doi="10.1007/3-540-12896-4_374",
url="http://dx.doi.org/10.1007/3-540-12896-4_374"
}
@Inbook{Hale1987,
author="Hale, Roger
and Moszkowski, Ben",
editor="de Bakker, J. W.
and Nijman, A. J.
and Treleaven, P. C.",
title="Parallel programming in Temporal Logic",
bookTitle="PARLE Parallel Architectures and Languages Europe: Volume II: Parallel Languages Eindhoven, The Netherlands, June 15--19, 1987 Proceedings",
year="1987",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="277--296",
isbn="978-3-540-47181-3",
doi="10.1007/3-540-17945-3_16",
url="http://dx.doi.org/10.1007/3-540-17945-3_16"
}
@inproceedings{Moszkowski:1994:VCT:647320.721175,
 author = {Moszkowski, Ben C.},
 title = {Some Very Compositional Temporal Properties},
 booktitle = {Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi},
 series = {PROCOMET '94},
 year = {1994},
 isbn = {0-444-82020-5},
 pages = {307--326},
 numpages = {20},
 url = {http://dl.acm.org/citation.cfm?id=647320.721175},
 acmid = {721175},
 publisher = {North-Holland Publishing Co.},
 address = {Amsterdam, The Netherlands, The Netherlands},
} 
@INPROCEEDINGS{479336, 
author={B. Moszkowski}, 
booktitle={Engineering of Complex Computer Systems, 1995. Held jointly with 5th CSESAW, 3rd IEEE RTAW and 20th IFAC/IFIP WRTP, Proceedings., First IEEE International Conference on}, 
title={Compositional reasoning about projected and infinite time}, 
year={1995}, 
pages={238-245}, 
keywords={concurrency control;multiprocessing systems;parallel programming;temporal logic;theorem proving;Interval Temporal Logic;assumptions;commitments;concurrency;concurrent system;deadlock;multiple time granularities;temporal logic;Concurrent computing;Internet;Logic;Safety;System recovery}, 
doi={10.1109/ICECCS.1995.479336}, 
month={Nov},
}
@Inbook{Moszkowski1998,
author="Moszkowski, B. C.",
editor="de Roever, Willem-Paul
and Langmaack, Hans
and Pnueli, Amir",
title="Compositional Reasoning using Interval Temporal Logic and Tempura",
bookTitle="Compositionality: The Significant Difference: International Symposium, COMPOS'97 Bad Malente, Germany, September 8--12, 1997 Revised Lectures",
year="1998",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="439--464",
isbn="978-3-540-49213-9",
doi="10.1007/3-540-49213-5_17",
url="http://dx.doi.org/10.1007/3-540-49213-5_17"
}
@Inbook{Moszkowski2000,
author="Moszkowski, Ben C.",
editor="Montanari, Ugo
and Rolim, Jos{\'e} D. P.
and Welzl, Emo",
title="An Automata-Theoretic Completeness Proof for Interval Temporal Logic",
bookTitle="Automata, Languages and Programming: 27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9--15, 2000 Proceedings",
year="2000",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="223--234",
isbn="978-3-540-45022-1",
doi="10.1007/3-540-45022-X_19",
url="http://dx.doi.org/10.1007/3-540-45022-X_19"
}
@INPROCEEDINGS{855773, 
author={B. C. Moszkowski}, 
booktitle={Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332)}, 
title={A complete axiomatization of interval temporal logic with infinite time}, 
year={2000}, 
pages={241-252}, 
keywords={computational complexity;finite state machines;temporal logic;temporal reasoning;theorem proving;ω-regular expressions;ITL formulas;axiom system;complete axiomatization;completeness proving;finite domains;finite-state automata;infinite sequential iteration;infinite time;interval temporal logic;quantified ITL;simple ITL deductive system;temporal reasoning;time periods;Automata;Calculus;Chaos;Logic;Reactive power;Real time systems}, 
doi={10.1109/LICS.2000.855773}, 
ISSN={1043-6871}, 
month={},
}
@Inbook{Moszkowski2003,
author="Moszkowski, Ben",
editor="Dershowitz, Nachum",
title="A Hierarchical Completeness Proof for Propositional Temporal Logic",
bookTitle="Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday",
year="2003",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="480--523",
isbn="978-3-540-39910-0",
doi="10.1007/978-3-540-39910-0_22",
url="http://dx.doi.org/10.1007/978-3-540-39910-0_22"
}
@INPROCEEDINGS{6065235, 
author={B. Moszkowski}, 
booktitle={2011 Eighteenth International Symposium on Temporal Representation and Reasoning}, 
title={Compositional Reasoning Using Intervals and Time Reversal}, 
year={2011}, 
pages={107-114}, 
keywords={inference mechanisms;temporal logic;compositional reasoning;concurrent behaviour;interval temporal logic;mutual exclusion;time reversal;Algorithm design and analysis;Analytical models;Argon;Cognition;Safety;Semantics;Syntactics;Interval Temporal Logic;Peterson's algorithm;compositional reasoning;formal verification;mutual exclusion}, 
doi={10.1109/TIME.2011.25}, 
ISSN={1530-1311}, 
month={Sept},
}
@Inbook{Moszkowski2015,
author="Moszkowski, Ben
and Guelev, Dimitar P.",
editor="Li, Xuandong
and Liu, Zhiming
and Yi, Wang",
title="An Application of Temporal Projection to Interleaving Concurrency",
bookTitle="Dependable Software Engineering: Theories, Tools, and Applications: First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings",
year="2015",
publisher="Springer International Publishing",
address="Cham",
pages="153--167",
isbn="978-3-319-25942-0",
doi="10.1007/978-3-319-25942-0_10",
url="http://dx.doi.org/10.1007/978-3-319-25942-0_10"
}
@inproceedings{Dwyer:1998:PSP:298595.298598,
 author = {Dwyer, Matthew B. and Avrunin, George S. and Corbett, James C.},
 title = {Property Specification Patterns for Finite-state Verification},
 booktitle = {Proceedings of the Second Workshop on Formal Methods in Software Practice},
 series = {FMSP '98},
 year = {1998},
 isbn = {0-89791-954-8},
 location = {Clearwater Beach, Florida, USA},
 pages = {7--15},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/298595.298598},
 doi = {10.1145/298595.298598},
 acmid = {298598},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrent systems, finite-state verification, formal specification, patterns},
} 
@INPROCEEDINGS{1553580, 
author={S. Konrad and B. H. C. Cheng}, 
booktitle={Proceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005.}, 
title={Real-time specification patterns}, 
year={2005}, 
pages={372-381}, 
keywords={embedded systems;formal specification;temporal logic;embedded systems;formal specification;pervasive system;real-time specification patterns;real-time temporal logics;structured English grammar;Automotive engineering;Computer science;Embedded software;Embedded system;Formal specifications;Laboratories;Logic;Permission;Real time systems;Software engineering}, 
doi={10.1109/ICSE.2005.1553580}, 
ISSN={0270-5257}, 
month={May},
}
@INPROCEEDINGS{841031, 
author={M. B. Dwyer and G. S. Avrunin and J. C. Corbett}, 
booktitle={Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002)}, 
title={Patterns in property specifications for finite-state verification}, 
year={1999}, 
pages={411-420}, 
keywords={formal specification;formal verification;object-oriented methods;automatic error detection;finite-state verification;formal methods;model checkers;property specification codification;property specification patterns;property specification presentation;property specification reuse;Automation;Computer errors;Computer science;Formal specifications;Logic;Mathematics;NASA;Permission;Statistics;System testing}, 
doi={10.1145/302405.302672}, 
ISSN={0270-5257}, 
month={May},
}
@Inbook{Moszkowski2015,
author="Moszkowski, Ben
and Guelev, Dimitar P.",
editor="Li, Xuandong
and Liu, Zhiming
and Yi, Wang",
title="An Application of Temporal Projection to Interleaving Concurrency",
bookTitle="Dependable Software Engineering: Theories, Tools, and Applications: First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings",
year="2015",
publisher="Springer International Publishing",
address="Cham",
pages="153--167",
isbn="978-3-319-25942-0",
doi="10.1007/978-3-319-25942-0_10",
url="http://dx.doi.org/10.1007/978-3-319-25942-0_10"
}
@inproceedings{Raimondi:2008:EOM:1453101.1453125,
 author = {Raimondi, Franco and Skene, James and Emmerich, Wolfgang},
 title = {Efficient Online Monitoring of Web-service SLAs},
 booktitle = {Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering},
 series = {SIGSOFT '08/FSE-16},
 year = {2008},
 isbn = {978-1-59593-995-1},
 location = {Atlanta, Georgia},
 pages = {170--180},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1453101.1453125},
 doi = {10.1145/1453101.1453125},
 acmid = {1453125},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {on-line monitoring, service level agreements, services},
} 
@INPROCEEDINGS{5341654, 
author={S. Kallel and A. Charfi and T. Dinkelaker and M. Mezini and M. Jmaiel}, 
booktitle={2009 Seventh IEEE European Conference on Web Services}, 
title={Specifying and Monitoring Temporal Properties in Web Services Compositions}, 
year={2009}, 
pages={148-157}, 
keywords={Web services;formal languages;formal specification;formal verification;object-oriented programming;system monitoring;AO4BPEL aspect;Web services composition;XTUS-Automata-expressive formal language;aspect-oriented programming;formal method;formal specification;modular enforcement code;temporal constraint runtime monitoring;verifiable temporal property specification;Computerized monitoring;Electronic mail;Formal languages;Formal specifications;Laboratories;Logic design;Quality of service;Runtime;System recovery;Web services;Aspect-oriented programming;Formal methods;Runtime monitoring;Temporal Properties;Web services}, 
doi={10.1109/ECOWS.2009.15}, 
month={Nov},
}
@ARTICLE{4907003, 
author={S. Halle and R. Villemaire and O. Cherkaoui}, 
journal={IEEE Transactions on Software Engineering}, 
title={Specifying and Validating Data-Aware Temporal Web Service Properties}, 
year={2009}, 
volume={35}, 
number={5}, 
pages={669-683}, 
keywords={Web services;computational complexity;formal specification;program verification;temporal logic;trees (mathematics);CTL-FO+;PSPACE-complete;computation tree logic;data-aware temporal Web service property;first-order quantification;formal specification;messages exchange;model checking algorithm complexity;syntactical checking;workflow validation;Web services;model checking;software/program verification;temporal logic.}, 
doi={10.1109/TSE.2009.29}, 
ISSN={0098-5589}, 
month={Sept},
}
@article{GRUHN2006117,
title = "Patterns for Timed Property Specifications",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "153",
number = "2",
pages = "117 - 133",
year = "2006",
note = "Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005)",
issn = "1571-0661",
doi = "http://dx.doi.org/10.1016/j.entcs.2005.10.035",
url = "http://www.sciencedirect.com/science/article/pii/S1571066106002623",
author = "Volker Gruhn and Ralf Laue",
keywords = "patterns",
keywords = "formal specification",
keywords = "real-time",
keywords = "verification"
}
@article{SHABTAI20101524,
title = "Intrusion detection for mobile devices using the knowledge-based, temporal abstraction method",
journal = "Journal of Systems and Software",
volume = "83",
number = "8",
pages = "1524 - 1537",
year = "2010",
note = "Performance Evaluation and Optimization of Ubiquitous Computing and Networked Systems",
issn = "0164-1212",
doi = "http://dx.doi.org/10.1016/j.jss.2010.03.046",
url = "http://www.sciencedirect.com/science/article/pii/S0164121210000762",
author = "Asaf Shabtai and Uri Kanonov and Yuval Elovici",
keywords = "Intrusion detection",
keywords = "Mobile devices",
keywords = "Temporal reasoning",
keywords = "Knowledge-based systems",
keywords = "Malware",
keywords = "Android"
}
@ARTICLE{6524462, 
author={M. H. Bhuyan and D. K. Bhattacharyya and J. K. Kalita}, 
journal={IEEE Communications Surveys Tutorials}, 
title={Network Anomaly Detection: Methods, Systems and Tools}, 
year={2014}, 
volume={16}, 
number={1}, 
pages={303-336}, 
keywords={Internet;computer network security;network anomaly detection;network defenders;network intrusion detection methods;network intrusion detection systems;Computational modeling;Computer architecture;Computers;Intrusion detection;Monitoring;Sun;Anomaly detection;NIDS;attack;classifier;dataset;intrusion detection;tools}, 
doi={10.1109/SURV.2013.052213.00046}, 
ISSN={1553-877X}, 
month={First},
}
@INPROCEEDINGS{5694933, 
author={H. Yong and Z. X. Feng}, 
booktitle={2010 3rd International Conference on Information Management, Innovation Management and Industrial Engineering}, 
title={Expert System Based Intrusion Detection System}, 
year={2010}, 
volume={4}, 
pages={404-407}, 
keywords={expert systems;feature extraction;principal component analysis;security of data;IPCA algorithm;data stream classification;expert system;intrusion detection system;kernel principal component analysis;nonlinear transformation scheme;unsupervised nonlinear feature extraction;Dimensionality reduction;expert system;incremental kernel PCA;recurrent multilayered perception}, 
doi={10.1109/ICIII.2010.578}, 
ISSN={2155-1456}, 
month={Nov},
}
@ARTICLE{279189, 
author={A. G. Parlos and K. T. Chong and A. F. Atiya}, 
journal={IEEE Transactions on Neural Networks}, 
title={Application of the recurrent multilayer perceptron in modeling complex process dynamics}, 
year={1994}, 
volume={5}, 
number={2}, 
pages={255-266}, 
keywords={feedforward neural nets;heat exchangers;large-scale systems;modelling;nonlinear dynamical systems;recurrent neural nets;approximate prediction;complex process dynamics modeling;dynamic gradient descent learning;heat exchanger;input-output modeling;moving average response;nonlinear dynamic model;online learning;ramps;recurrent multilayer perceptron;steps;Artificial neural networks;Intelligent networks;Multi-layer neural network;Multilayer perceptrons;Neural networks;Nonlinear dynamical systems;Power engineering and energy;Predictive models;Signal processing;Testing}, 
doi={10.1109/72.279189}, 
ISSN={1045-9227}, 
month={Mar},
}
@article{HERRERO2013250,
title = "RT-MOVICAB-IDS: Addressing real-time intrusion detection",
journal = "Future Generation Computer Systems",
volume = "29",
number = "1",
pages = "250 - 261",
year = "2013",
note = "Including Special section: AIRCC-NetCoM 2009 and Special section: Clouds and Service-Oriented Architectures",
issn = "0167-739X",
doi = "http://dx.doi.org/10.1016/j.future.2010.12.017",
url = "http://www.sciencedirect.com/science/article/pii/S0167739X10002785",
author = "Álvaro Herrero and Martí Navarro and Emilio Corchado and Vicente Julián",
keywords = "Hybrid Artificial Intelligent Systems",
keywords = "Unsupervised learning",
keywords = "Artificial Neural Networks",
keywords = "Multi-Agent systems",
keywords = "Case-based reasoning",
keywords = "Computer network security",
keywords = "Intrusion detection",
keywords = "Time-bounded deliberative process"
}
@inproceedings{Spanoudakis:2007:TSM:1244002.1244327,
 author = {Spanoudakis, George and Kloukinas, Christos and Androutsopoulos, Kelly},
 title = {Towards Security Monitoring Patterns},
 booktitle = {Proceedings of the 2007 ACM Symposium on Applied Computing},
 series = {SAC '07},
 year = {2007},
 isbn = {1-59593-480-4},
 location = {Seoul, Korea},
 pages = {1518--1525},
 numpages = {8},
 url = {http://doi.acm.org/10.1145/1244002.1244327},
 doi = {10.1145/1244002.1244327},
 acmid = {1244327},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {event calculus, runtime monitoring, security patterns},
} 
@inproceedings{Dwyer:1998:PSP:298595.298598,
 author = {Dwyer, Matthew B. and Avrunin, George S. and Corbett, James C.},
 title = {Property Specification Patterns for Finite-state Verification},
 booktitle = {Proceedings of the Second Workshop on Formal Methods in Software Practice},
 series = {FMSP '98},
 year = {1998},
 isbn = {0-89791-954-8},
 location = {Clearwater Beach, Florida, USA},
 pages = {7--15},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/298595.298598},
 doi = {10.1145/298595.298598},
 acmid = {298598},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrent systems, finite-state verification, formal specification, patterns},
} 
@inproceedings{Sommer:2014er,
 author = {Sommer, Robin and Vallentin, Matthias and De Carli, Lorenzo and Paxson, Vern},
 title = {HILTI: An Abstract Execution Environment for Deep, Stateful Network Traffic Analysis},
 booktitle = {Proceedings of the 2014 Conference on Internet Measurement Conference},
 series = {IMC '14},
 year = {2014},
 isbn = {978-1-4503-3213-2},
 location = {Vancouver, BC, Canada},
 pages = {461--474},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2663716.2663735},
 doi = {10.1145/2663716.2663735},
 acmid = {2663735},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {deep packet inspection, intrusion detection, real-time monitoring},
} 

@article{Shiravi:2012hr,
  title={Toward Developing a Dystematic Approach to Generate Benchmark Datasets for Intrusion Tetection},
  author={Shiravi, Ali and Shiravi, Hadi and Tavallaee, Mahbod and Ghorbani, Ali A},
  journal={Computers \& Security},
  volume={31},
  number={3},
  pages={357--374},
  year={2012},
  publisher={Elsevier}
}

@inproceedings{DeCarli:2014:BPM:2660267.2660361,
 author = {De Carli, Lorenzo and Sommer, Robin and Jha, Somesh},
 title = {Beyond Pattern Matching: A Concurrency Model for Stateful Deep Packet Inspection},
 booktitle = {Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security},
 series = {CCS '14},
 year = {2014},
 isbn = {978-1-4503-2957-6},
 location = {Scottsdale, Arizona, USA},
 pages = {1378--1390},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2660267.2660361},
 doi = {10.1145/2660267.2660361},
 acmid = {2660361},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {flexible intrusion detection, nids, scalable traffic analysis},
} 

@inproceedings{vallentin2016vast,
author = {Matthias Vallentin and Vern Paxson and Robin Sommer},
title = {VAST: A Unified Platform for Interactive Network Forensics},
booktitle = {13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16)},
year = {2016},
month = Mar,
isbn = {978-1-931971-29-4},
address = {Santa Clara, CA},
pages = {345--362},
url = {https://www.usenix.org/conference/nsdi16/technical-sessions/presentation/vallentin},
publisher = {USENIX Association},
} 

@article{liao2013intrusion,
  title={Intrusion Detection System: A Comprehensive Review},
  author={Liao, Hung-Jen and Lin, Chun-Hung Richard and Lin, Ying-Chih and Tung, Kuang-Yuan},
  journal={Journal of Network and Computer Applications},
  volume={36},
  number={1},
  pages={16--24},
  year={2013},
  publisher={Elsevier}
}

@inproceedings{Ning:2003:LAS:948109.948137,
 author = {Ning, Peng and Xu, Dingbang},
 title = {Learning Attack Strategies from Intrusion Alerts},
 booktitle = {Proceedings of the 10th ACM Conference on Computer and Communications Security},
 series = {CCS '03},
 year = {2003},
 isbn = {1-58113-738-9},
 location = {Washington D.C., USA},
 pages = {200--209},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/948109.948137},
 doi = {10.1145/948109.948137},
 acmid = {948137},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {alert correlation, intrusion detection, profiling attack strategies},
} 

@inproceedings{1004372, 
author={F. Cuppens and A. Miege}, 
booktitle={Proceedings 2002 IEEE Symposium on Security and Privacy}, 
title={Alert Correlation in a Cooperative Intrusion Detection Framework}, 
year={2002}, 
pages={202-215}, 
keywords={authorisation;CRIM;MIRADOR project;alert clustering;alert correlation;alert management;alert merging;cooperative intrusion detection framework;global alerts;synthetic alerts;Collaboration;Data security;Dissolved gas analysis;Information security;Intrusion detection;Laboratories;Merging;Pattern matching}, 
doi={10.1109/SECPRI.2002.1004372}, 
ISSN={1081-6011}, 
month={},}

@inproceedings{viswanathan2011semantic,
  title={A Semantic Framework for Data Analysis in Networked Systems},
  author={Viswanathan, Arun and Hussain, Alefiya and Mirkovic, Jelena and Schwab, Stephen and Wroclawski, John},
  booktitle={Proceedings of NSDI’11: 8th USENIX Symposium on Networked Systems Design and Implementation},
  pages={127},
  year={2011},
  organization={Citeseer}
}
@article{Lamport:1994:TLA:177492.177726,
 author = {Lamport, Leslie},
 title = {The Temporal Logic of Actions},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {May 1994},
 volume = {16},
 number = {3},
 month = may,
 year = {1994},
 issn = {0164-0925},
 pages = {872--923},
 numpages = {52},
 url = {http://doi.acm.org/10.1145/177492.177726},
 doi = {10.1145/177492.177726},
 acmid = {177726},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrent programming, liveness properties, safety properties},
} 
@article{Allen:1983:MKT:182.358434,
 author = {Allen, James F.},
 title = {Maintaining Knowledge About Temporal Intervals},
 journal = {Commun. ACM},
 issue_date = {Nov. 1983},
 volume = {26},
 number = {11},
 month = nov,
 year = {1983},
 issn = {0001-0782},
 pages = {832--843},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/182.358434},
 doi = {10.1145/182.358434},
 acmid = {358434},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {interval reasoning, interval representation, temporal interval},
} 
@inproceedings{Hewitt:1973:UMA:1624775.1624804,
 author = {Hewitt, Carl and Bishop, Peter and Steiger, Richard},
 title = {A Universal Modular ACTOR Formalism for Artificial Intelligence},
 booktitle = {Proceedings of the 3rd International Joint Conference on Artificial Intelligence},
 series = {IJCAI'73},
 year = {1973},
 location = {Stanford, USA},
 pages = {235--245},
 numpages = {11},
 url = {http://dl.acm.org/citation.cfm?id=1624775.1624804},
 acmid = {1624804},
 publisher = {Morgan Kaufmann Publishers Inc.},
 address = {San Francisco, CA, USA},
} 
@incollection{hoare1978communicating,
  title={Communicating sequential processes},
  author={Hoare, Charles Antony Richard},
  booktitle={The origin of concurrent programming},
  pages={413--443},
  year={1978},
  publisher={Springer}
}
@inproceedings {raft:2014,
author = {Diego Ongaro and John Ousterhout},
title = {In Search of an Understandable Consensus Algorithm},
booktitle = {2014 USENIX Annual Technical Conference (USENIX ATC 14)},
year = {2014},
month = Jun,
isbn = {978-1-931971-10-2},
address = {Philadelphia, PA},
pages = {305--319},
url = {https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro},
publisher = {USENIX Association},
}

@article{lirui2015,
  title={一种密闭可重构网络安全测试床的设计与实现},
  author={李睿 and 朱俊虎 and 王清贤 and 周天阳 },
  journal={信息工程大学学报},
  volume={16},
  number={1},
  pages={111--116},
  year={2015}
}
@inproceedings{Roger:2001:LAT:872752.873518,
 author = {Roger, Muriel and Goubault-Larrecq, Jean},
 title = {Log Auditing Through Model-Checking},
 booktitle = {Proceedings of the 14th IEEE Workshop on Computer Security Foundations},
 series = {CSFW '01},
 year = {2001},
 pages = {220--},
 url = {http://dl.acm.org/citation.cfm?id=872752.873518},
 acmid = {873518},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
} 
@inproceedings{Ellis:2004:BAW:1029618.1029625,
 author = {Ellis, Daniel R. and Aiken, John G. and Attwood, Kira S. and Tenaglia, Scott D.},
 title = {A Behavioral Approach to Worm Detection},
 booktitle = {Proceedings of the 2004 ACM Workshop on Rapid Malcode},
 series = {WORM '04},
 year = {2004},
 isbn = {1-58113-970-5},
 location = {Washington DC, USA},
 pages = {43--53},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1029618.1029625},
 doi = {10.1145/1029618.1029625},
 acmid = {1029625},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {behavioral signatures, descendant relation, intrusion detection, network application architecture, network worms},
} 
@inproceedings{Kinder05detectingmalicious,
    author = {Johannes Kinder and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith and Technische Universität München},
    title = {Detecting malicious code by model checking},
    booktitle = {Proceedings of the 2nd International Conference on Intrusion and Malware Detection and Vulnerability Assessment (DIMVA’05), volume 3548 of Lecture Notes in Computer Science},
    year = {2005},
    pages = {174--187},
    publisher = {Springer Berlin}
}
@Inbook{Naldurg2004,
author={Naldurg, Prasad
and Sen, Koushik
and Thati, Prasanna},
editor={de Frutos-Escrig, David and N{\'u}{\~{n}}ez, Manuel},
title={A Temporal Logic Based Framework for Intrusion Detection},
bookTitle={Formal Techniques for Networked and Distributed Systems -- FORTE 2004: 24th IFIP WG 6.1 International Conference, Madrid Spain, September 27-30, 2004. Proceedings},
year={2004},
publisher={Springer Berlin Heidelberg},
address={Berlin, Heidelberg},
pages={359--376},
isbn={978-3-540-30232-2},
doi={10.1007/978-3-540-30232-2_23},
url={http://dx.doi.org/10.1007/978-3-540-30232-2_23}
}
@article{Basin:2013:MDU:2554420.2554425,
 author = {Basin, David and Harvan, Matus and Klaedtke, Felix and Z\v{a}linescu, Eugen},
 title = {Monitoring Data Usage in Distributed Systems},
 journal = {IEEE Trans. Softw. Eng.},
 issue_date = {October 2013},
 volume = {39},
 number = {10},
 month = oct,
 year = {2013},
 issn = {0098-5589},
 pages = {1403--1426},
 numpages = {24},
 url = {http://dx.doi.org/10.1109/TSE.2013.18},
 doi = {10.1109/TSE.2013.18},
 acmid = {2554425},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 keywords = {regulation,Monitors,temporal logic,verification,distributed systems},
}
@article{Marchetti2016127,
title = "Analysis of high volumes of network traffic for Advanced Persistent Threat detection ",
journal = "Computer Networks ",
volume = "109, Part 2",
number = "",
pages = "127 - 141",
year = "2016",
note = "Traffic and Performance in the Big Data Era ",
issn = "1389-1286",
doi = "http://dx.doi.org/10.1016/j.comnet.2016.05.018",
url = "http://www.sciencedirect.com/science/article/pii/S1389128616301633",
author = "Mirco Marchetti and Fabio Pierazzi and Michele Colajanni and Alessandro Guido",
keywords = "Security analytics",
keywords = "Traffic analysis",
keywords = "Advanced Persistent Threats",
keywords = "Data exfiltration "
}
@inproceedings{Bersani:2016:ELT:2884781.2884832,
 author = {Bersani, Marcello M. and Bianculli, Domenico and Ghezzi, Carlo and Krsti\'{c}, Sr\&\#273;an and Pietro, Pierluigi San},
 title = {Efficient Large-scale Trace Checking Using Mapreduce},
 booktitle = {Proceedings of the 38th International Conference on Software Engineering},
 series = {ICSE '16},
 year = {2016},
 isbn = {978-1-4503-3900-1},
 location = {Austin, Texas},
 pages = {888--898},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/2884781.2884832},
 doi = {10.1145/2884781.2884832},
 acmid = {2884832},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@article{Basin:2015:MMF:2772377.2699444,
 author = {Basin, David and Klaedtke, Felix and M\"{u}ller, Samuel and Z\u{a}linescu, Eugen},
 title = {Monitoring Metric First-Order Temporal Properties},
 journal = {J. ACM},
 issue_date = {May 2015},
 volume = {62},
 number = {2},
 month = may,
 year = {2015},
 issn = {0004-5411},
 pages = {15:1--15:45},
 articleno = {15},
 numpages = {45},
 url = {http://doi.acm.org/10.1145/2699444},
 doi = {10.1145/2699444},
 acmid = {2699444},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Runtime verification, automatic structures, compliance checking, security policies, temporal databases},
} 
@INPROCEEDINGS{johnson2013, 
author={J. R. Johnson and E. A. Hogan}, 
booktitle={2013 IEEE International Conference on Intelligence and Security Informatics}, 
title={A graph analytic metric for mitigating advanced persistent threat}, 
year={2013}, 
pages={129-133}, 
keywords={authorisation;computer network security;graph theory;advanced persistent threat mitigation;auditing layers;authorization layers;cyber network vulnerability;edge selection;edge vertices;graph analytic metrics;lateral movement;network security authorization phase;node selection;oriented subgraph;predictive deterrence;privilege escalation;Authentication;Authorization;Graph theory;Heuristic algorithms;Measurement;Presses;cybersecurity;discrete mathematics;graph theory}, 
doi={10.1109/ISI.2013.6578801}, 
month={June},}
@article{Friedberg201535,
title = {Combating advanced persistent threats: From network event correlation to incident detection},
journal = {Computers \& Security},
volume = "48",
number = "",
pages = "35 - 57",
year = "2015",
note = "",
issn = "0167-4048",
doi = "http://dx.doi.org/10.1016/j.cose.2014.09.006",
url = "http://www.sciencedirect.com/science/article/pii/S0167404814001461",
author = "Ivo Friedberg and Florian Skopik and Giuseppe Settanni and Roman Fiedler",
keywords = "Advanced persistent threat",
keywords = "Anomaly detection",
keywords = "Log file analysis",
keywords = "Intrusion detection",
keywords = "Event correlation",
keywords = "Self-learning system model "
}
@article{Shiravi2012357,
title = "Toward developing a systematic approach to generate benchmark datasets for intrusion detection ",
journal = {Computers \& Security},
volume = "31",
number = "3",
pages = "357 - 374",
year = "2012",
note = "",
issn = "0167-4048",
doi = "http://dx.doi.org/10.1016/j.cose.2011.12.012",
url = "http://www.sciencedirect.com/science/article/pii/S0167404811001672",
author = "Ali Shiravi and Hadi Shiravi and Mahbod Tavallaee and Ali A. Ghorbani",
keywords = "Intrusion detection",
keywords = "Dataset generation",
keywords = "Network traffic profile "
}
@article{García2014100,
title = "An empirical comparison of botnet detection methods ",
journal = {Computers \& Security },
volume = "45",
number = "",
pages = "100 - 123",
year = "2014",
note = "",
issn = "0167-4048",
doi = "http://dx.doi.org/10.1016/j.cose.2014.05.011",
url = "http://www.sciencedirect.com/science/article/pii/S0167404814000923",
author = "S. García and M. Grill and J. Stiborek and A. Zunino",
keywords = "Botnet detection",
keywords = "Malware detection",
keywords = "Methods comparison",
keywords = "Botnet dataset",
keywords = "Anomaly detection",
keywords = "Network traffic "
}
@ARTICLE{igure2008, 
author={V. M. Igure and R. D. Williams}, 
journal={IEEE Communications Surveys Tutorials}, 
title={Taxonomies of attacks and vulnerabilities in computer systems}, 
year={2008}, 
volume={10}, 
number={1}, 
pages={6-19}, 
keywords={telecommunication security;computer system attacks;computer system vulnerabilities;information organization;security assessment;taxonomies;Buildings;Communication system security;Data security;Databases;Information security;Organizing;Standards publication;Taxonomy}, 
doi={10.1109/COMST.2008.4483667}, 
ISSN={1553-877X}, 
month={First},}
@article{Meng:2015:CSS:2808687.2785733,
 author = {Meng, Guozhu and Liu, Yang and Zhang, Jie and Pokluda, Alexander and Boutaba, Raouf},
 title = {Collaborative Security: A Survey and Taxonomy},
 journal = {ACM Comput. Surv.},
 issue_date = {September 2015},
 volume = {48},
 number = {1},
 month = jul,
 year = {2015},
 issn = {0360-0300},
 pages = {1:1--1:42},
 articleno = {1},
 numpages = {42},
 url = {http://doi.acm.org/10.1145/2785733},
 doi = {10.1145/2785733},
 acmid = {2785733},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Collaborative security, information sharing, intrusion detection, malware, privacy, spam, taxonomy, trust},
} 
@article{Ahmed:2016:SNA:2894395.2894710,
 author = {Ahmed, Mohiuddin and Naser Mahmood, Abdun and Hu, Jiankun},
 title = {A Survey of Network Anomaly Detection Techniques},
 journal = {J. Netw. Comput. Appl.},
 issue_date = {January 2016},
 volume = {60},
 number = {C},
 month = jan,
 year = {2016},
 issn = {1084-8045},
 pages = {19--31},
 numpages = {13},
 url = {http://dx.doi.org/10.1016/j.jnca.2015.11.016},
 doi = {10.1016/j.jnca.2015.11.016},
 acmid = {2894710},
 publisher = {Academic Press Ltd.},
 address = {London, UK, UK},
 keywords = {Anomaly detection, Classification, Clustering, Computer security, Information theory, Intrusion detection},
} 
@article{Liao:2013:RID:2405859.2406209,
 author = {Liao, Hung-Jen and Richard Lin, Chun-Hung and Lin, Ying-Chih and Tung, Kuang-Yuan},
 title = {Review: Intrusion Detection System: A Comprehensive Review},
 journal = {J. Netw. Comput. Appl.},
 issue_date = {January, 2013},
 volume = {36},
 number = {1},
 month = jan,
 year = {2013},
 issn = {1084-8045},
 pages = {16--24},
 numpages = {9},
 url = {http://dx.doi.org/10.1016/j.jnca.2012.09.004},
 doi = {10.1016/j.jnca.2012.09.004},
 acmid = {2406209},
 publisher = {Academic Press Ltd.},
 address = {London, UK, UK},
 keywords = {Anomaly, Intrusion detection, Misuse},
} 
@article{Khan2016,
  author = {Khan, Suleman and Gani, Abdullah and Wahab, Ainuddin Wahid Abdul and Shiraz, Muhammad and Ahmad, Iftikhar},
  doi = {10.1016/j.jnca.2016.03.005},
  journal = {Journal of Network and Computer Applications},
  keywords = {Forensic; Investigation; Cybercrimes; Digital evidence; Intrusion detection},
  language = {English},
  number = {Complete},
  pages = {214-235},
  title = {Review},
  volume = {66},
  year = {2016},
}
@ARTICLE{7029714, 
author={M. Autili and L. Grunske and M. Lumpe and P. Pelliccione and A. Tang}, 
journal={IEEE Transactions on Software Engineering}, 
title={Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar}, 
year={2015}, 
volume={41}, 
number={7}, 
pages={620-638}, 
keywords={formal specification;natural language processing;probability;temporal logic;PSPWizard;event probability;event qualitative aspect;event quantitative aspect;formal methods;mathematical reasoning;natural language front-end;occurrence qualification;order qualification;pattern mapping;probabilistic property specification pattern;qualitative property specification pattern;real-time property specification pattern;software system correctness;structured English grammar;temporal intricacies;temporal logic;time bound quantification;unified pattern catalogue;Educational institutions;Electronic mail;Grammar;Natural languages;Probabilistic logic;Real-time systems;Software;Probabilistic Properties;Real-time Properties;Specification Patterns;Specification patterns;probabilistic properties;real-time properties}, 
doi={10.1109/TSE.2015.2398877}, 
ISSN={0098-5589}, 
month={July},
}
@INPROCEEDINGS{777992, 
author={D. O. Paun and M. Chechik}, 
booktitle={Proceedings IEEE International Symposium on Requirements Engineering (Cat. No.PR00188)}, 
title={Events in linear-time properties}, 
year={1999}, 
pages={123-132}, 
keywords={algebraic specification;formal verification;temporal logic;PSPACE-complete;formal methods;formal specification;linear-time properties;linear-time temporal logic;mathematical reasoning;partial-order reduction technique;reasoning tools;stuttering;syntactic reasoning;verification tools;Algebra;Algorithm design and analysis;Computer science;Concurrent computing;Cranes;Logic functions;Magnetic properties;Power system modeling;State-space methods}, 
doi={10.1109/ISRE.1999.777992}, 
month={},
}
@inproceedings{Smith:2002:PAS:581339.581345,
 author = {Smith, Rachel L. and Avrunin, George S. and Clarke, Lori A. and Osterweil, Leon J.},
 title = {PROPEL: An Approach Supporting Property Elucidation},
 booktitle = {Proceedings of the 24th International Conference on Software Engineering},
 series = {ICSE '02},
 year = {2002},
 isbn = {1-58113-472-X},
 location = {Orlando, Florida},
 pages = {11--21},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/581339.581345},
 doi = {10.1145/581339.581345},
 acmid = {581345},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@Inbook{Castillos2013,
author="Castillos, Kalou Cabrera
and Dadeau, Fr{\'e}d{\'e}ric
and Julliand, Jacques
and Kanso, Bilal
and Taha, Safouan",
editor="Johnsen, Einar Broch
and Petre, Luigia",
title="A Compositional Automata-Based Semantics for Property Patterns",
bookTitle="Integrated Formal Methods: 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="316--330",
abstract="Dwyer et al. define a language to specify dynamic properties based on predefined patterns and scopes. To define a property, the user has to choose a pattern and a scope among a limited number of them. Dwyer et al. define the semantics of these properties by translating each composition of a pattern and a scope into usual temporal logics (LTL, CTL, etc.). First, this translational semantics is not compositional and thus not easily extensible to other patterns/scopes. Second, it is not always faithful to the natural semantics of the informal definitions.",
isbn="978-3-642-38613-8",
doi="10.1007/978-3-642-38613-8_22",
url="https://doi.org/10.1007/978-3-642-38613-8_22"
}
@ARTICLE{4907003, 
author={S. Halle and R. Villemaire and O. Cherkaoui}, 
journal={IEEE Transactions on Software Engineering}, 
title={Specifying and Validating Data-Aware Temporal Web Service Properties}, 
year={2009}, 
volume={35}, 
number={5}, 
pages={669-683}, 
keywords={Web services;computational complexity;formal specification;program verification;temporal logic;trees (mathematics);CTL-FO+;PSPACE-complete;computation tree logic;data-aware temporal Web service property;first-order quantification;formal specification;messages exchange;model checking algorithm complexity;syntactical checking;workflow validation;Web services;model checking;software/program verification;temporal logic.}, 
doi={10.1109/TSE.2009.29}, 
ISSN={0098-5589}, 
month={Sept},
}
@inproceedings{Bitsch:2001:SPK:647399.724860,
 author = {Bitsch, Friedemann},
 title = {Safety Patterns - The Key to Formal Specification of Safety Requirements},
 booktitle = {Proceedings of the 20th International Conference on Computer Safety, Reliability and Security},
 series = {SAFECOMP '01},
 year = {2001},
 isbn = {3-540-42607-8},
 pages = {176--189},
 numpages = {14},
 url = {http://dl.acm.org/citation.cfm?id=647399.724860},
 acmid = {724860},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 
@phdthesis{Alur:1992:TAV:143902,
 author = {Alur, Rajeev},
 title = {Techniques for Automatic Verification of Real-time Systems},
 year = {1992},
 note = {UMI Order No. GAX92-06729},
 publisher = {Stanford University},
 address = {Stanford, CA, USA},
} 
@Inbook{Abid2012,
author="Abid, Nouha
and Dal Zilio, Silvano
and Le Botlan, Didier",
editor="Stoelinga, Mari{\"e}lle
and Pinger, Ralf",
title="Real-Time Specification Patterns and Tools",
bookTitle="Formal Methods for Industrial Critical Systems: 17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings",
year="2012",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="1--15",
abstract="An issue limiting the adoption of model checking technologies by the industry is the ability, for non-experts, to express their requirements using the property languages supported by verification tools. This has motivated the definition of dedicated assertion languages for expressing temporal properties at a higher level. However, only a limited number of these formalisms support the definition of timing constraints. In this paper, we propose a set of specification patterns that can be used to express real-time requirements commonly found in the design of reactive systems. We also provide an integrated model checking tool chain for the verification of timed requirements on TTS, an extension of Time Petri Nets with data variables and priorities.",
isbn="978-3-642-32469-7",
doi="10.1007/978-3-642-32469-7_1",
url="https://doi.org/10.1007/978-3-642-32469-7_1"
}
@Inbook{Aziz1996,
author="Aziz, Adnan
and Sanwal, Kumud
and Singhal, Vigyan
and Brayton, Robert",
editor="Alur, Rajeev
and Henzinger, Thomas A.",
title="Verifying continuous time Markov chains",
bookTitle="Computer Aided Verification: 8th International Conference, CAV '96 New Brunswick, NJ, USA, July 31-- August 3, 1996 Proceedings",
year="1996",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="269--276",
abstract="We present a logical formalism for expressing properties of continuous time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete time Markov chains to continuous time. The major result is that the verification problem is decidable; this is shown using results in algebraic and transcendental number theory.",
isbn="978-3-540-68599-9",
doi="10.1007/3-540-61474-5_75",
url="https://doi.org/10.1007/3-540-61474-5_75"
}
@inproceedings{Cobleigh:2006:UGC:1181775.1181801,
 author = {Cobleigh, Rachel L. and Avrunin, George S. and Clarke, Lori A.},
 title = {User Guidance for Creating Precise and Accessible Property Specifications},
 booktitle = {Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering},
 series = {SIGSOFT '06/FSE-14},
 year = {2006},
 isbn = {1-59593-468-5},
 location = {Portland, Oregon, USA},
 pages = {208--218},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1181775.1181801},
 doi = {10.1145/1181775.1181801},
 acmid = {1181801},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {property specifications},
} 
@Article{Autili2007,
author="Autili, M.
and Inverardi, P.
and Pelliccione, P.",
title="Graphical scenarios for specifying temporal properties: an automated approach",
journal="Automated Software Engineering",
year="2007",
month="Sep",
day="01",
volume="14",
number="3",
pages="293--340",
abstract="Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically specified as linear-time formulae in temporal logics. Unfortunately, the level of inherent sophistication required by these formalisms too often represents an impediment to move these techniques from ``research theory'' to ``industry practice''. The objective of this work is to facilitate the nontrivial and error prone task of specifying, correctly and without expertise in temporal logic, temporal properties.",
issn="1573-7535",
doi="10.1007/s10515-007-0012-6",
url="https://doi.org/10.1007/s10515-007-0012-6"
}
@article{Autili:2008:TGT:1367148.1367347,
 author = {Autili, Marco and Pelliccione, Patrizio},
 title = {Towards a Graphical Tool for Refining User to System Requirements},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {April, 2008},
 volume = {211},
 month = apr,
 year = {2008},
 issn = {1571-0661},
 pages = {147--157},
 numpages = {11},
 url = {http://dx.doi.org/10.1016/j.entcs.2008.04.037},
 doi = {10.1016/j.entcs.2008.04.037},
 acmid = {1367347},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Graphical Formalisms, Requirements Definition, Software Architectures},
} 
@article{Zave:1997:FDC:237432.237434,
 author = {Zave, Pamela and Jackson, Michael},
 title = {Four Dark Corners of Requirements Engineering},
 journal = {ACM Trans. Softw. Eng. Methodol.},
 issue_date = {Jan. 1997},
 volume = {6},
 number = {1},
 month = jan,
 year = {1997},
 issn = {1049-331X},
 pages = {1--30},
 numpages = {30},
 url = {http://doi.acm.org/10.1145/237432.237434},
 doi = {10.1145/237432.237434},
 acmid = {237434},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {control of actions, domain knowledge, implementation bias, refinement of requirements},
} 
@INPROCEEDINGS{5431747, 
author={P. Zhang and L. Grunske and A. Tang and B. Li}, 
booktitle={2009 IEEE/ACM International Conference on Automated Software Engineering}, 
title={A Formal Syntax for Probabilistic Timed Property Sequence Charts}, 
year={2009}, 
pages={500-504}, 
keywords={probabilistic logic;specification languages;extrafunctional requirements;formal syntax;probabilistic logics;probabilistic timed property sequence charts;software developers;temporal logics;traffic accidents;vehicle-to-vehicle communication device;Computer aided instruction;Computer architecture;Concurrent computing;Heuristic algorithms;Information science;Java;Programming environments;Programming profession;Software engineering;Yarn;Probabilistic Properties;Probabilistic and Timed Property Sequence Chart;Property Sequence Chart}, 
doi={10.1109/ASE.2009.56}, 
ISSN={1938-4300}, 
month={Nov},
}
@article{ZHANG2010371,
title = "Timed Property Sequence Chart",
journal = "Journal of Systems and Software",
volume = "83",
number = "3",
pages = "371 - 390",
year = "2010",
note = "",
issn = "0164-1212",
doi = "http://dx.doi.org/10.1016/j.jss.2009.09.013",
url = "http://www.sciencedirect.com/science/article/pii/S0164121209002301",
author = "Pengcheng Zhang and Bixin Li and Lars Grunske",
keywords = "Property Sequence Chart",
keywords = "Timed Property Sequence Chart",
keywords = "Timing properties",
keywords = "Real-time specification patterns"
}
@INPROCEEDINGS{5647654, 
author={L. Di Guglielmo and F. Fummi and N. Orlandi and G. Pravadelli}, 
booktitle={2010 IEEE International Conference on Computer Design}, 
title={DDPSL: An easy way of defining properties}, 
year={2010}, 
pages={468-473}, 
keywords={formal specification;formal verification;specification languages;temporal logic;trees (mathematics);CTL;DDPSL;DUV;LTL;OVL;PSL-based templates;Property Specification Language;computational tree logic;design under verification;drag and drop PSL;formal methods;formal property;industrial oven;linear temporal logic;logical operator;microcontroller;open verification library;reference language;template library;temporal logics;temporal operator;Hardware;Hardware design languages;Libraries;Monitoring;Ovens;Semantics;Switches}, 
doi={10.1109/ICCD.2010.5647654}, 
ISSN={1063-6404}, 
month={Oct},
}
@book{Holzmann:2003:SMC:1405716,
 author = {Holzmann, Gerard},
 title = {Spin Model Checker, the: Primer and Reference Manual},
 year = {2003},
 isbn = {0-321-22862-6},
 edition = {First},
 publisher = {Addison-Wesley Professional},
} 
@Inbook{Capozucca2006,
author="Capozucca, Alfredo
and Guelfi, Nicolas
and Pelliccione, Patrizio",
editor="Butler, Michael
and Jones, Cliff B.
and Romanovsky, Alexander
and Troubitsyna, Elena",
title="The Fault-Tolerant Insulin Pump Therapy",
bookTitle="Rigorous Development of Complex Fault-Tolerant Systems",
year="2006",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="59--79",
abstract="The ``Fault-Tolerant Insulin Pump Therapy'' is based on the Continuous Subcutaneous Insulin Injection technique which combines devices (a sensor and a pump) and software in order to make glucose sensing and insulin delivery automatic. These devices are not physically connected together and they come with the necessary features to detect malfunctions which they may have.",
isbn="978-3-540-48267-3",
doi="10.1007/11916246_3",
url="https://doi.org/10.1007/11916246_3"
}
@book{Bozzano:2010:DSA:1951720,
 author = {Bozzano, Marco and Villafiorita, Adolfo},
 title = {Design and Safety Assessment of Critical Systems},
 year = {2010},
 isbn = {1439803315, 9781439803318},
 edition = {1st},
 publisher = {Auerbach Publications},
 address = {Boston, MA, USA},
} 
@article{BELLINI2009183,
title = "Expressing and organizing real-time specification patterns via temporal logics",
journal = "Journal of Systems and Software",
volume = "82",
number = "2",
pages = "183 - 196",
year = "2009",
note = "",
issn = "0164-1212",
doi = "http://dx.doi.org/10.1016/j.jss.2008.06.041",
url = "http://www.sciencedirect.com/science/article/pii/S0164121208001763",
author = "P. Bellini and P. Nesi and D. Rogai",
keywords = "Patterns",
keywords = "Real-time specification pattern",
keywords = "Formal methods",
keywords = "Temporal logic",
keywords = "TILCO"
}
@INPROCEEDINGS{1553580, 
author={S. Konrad and B. H. C. Cheng}, 
booktitle={Proceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005.}, 
title={Real-time specification patterns}, 
year={2005}, 
pages={372-381}, 
keywords={embedded systems;formal specification;temporal logic;embedded systems;formal specification;pervasive system;real-time specification patterns;real-time temporal logics;structured English grammar;Automotive engineering;Computer science;Embedded software;Embedded system;Formal specifications;Laboratories;Logic;Permission;Real time systems;Software engineering}, 
doi={10.1109/ICSE.2005.1553580}, 
ISSN={0270-5257}, 
month={May},
}
@INPROCEEDINGS{4814114, 
author={L. Grunske}, 
booktitle={2008 ACM/IEEE 30th International Conference on Software Engineering}, 
title={Specification patterns for probabilistic quality properties}, 
year={2008}, 
pages={31-40}, 
keywords={formal specification;formal verification;grammars;probabilistic logic;software quality;ProProST;formal verification;probabilistic quality properties;probabilistic verification;quality requirements;software-intensive system;specification patterns;structured English grammar;Aerospace electronics;Australia;Automotive engineering;Computer aided software engineering;Formal verification;Hazards;Permission;Probabilistic logic;Real time systems;Software engineering;csl;pctl;pctl*;performance;probabilistic quality;probabilistic quality patterns;reliability;safety;security;specification patterns}, 
doi={10.1145/1368088.1368094}, 
ISSN={0270-5257}, 
month={May},
}
@ARTICLE{5446004, 
journal={IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005)}, 
title={IEEE Standard for Property Specification Language (PSL)}, 
year={2010}, 
pages={1-182}, 
keywords={IEEE standards;formal languages;formal specification;formal verification;specification languages;IEEE Std 1076¿¿;IEEE Std 1354;IEEE Std 1666¿¿;IEEE Std 1800¿¿;IEEE property specification language;SystemC¿¿;SystemVerilog¿¿;VHDL¿¿;Verilog¿¿;electronic system design;electronic system specification;formal analysis;formal specification verification;formal verification flow;mixedlanguage designs;multilanguage designs;IEEE standards;Specification languages;1850-2010;ABV;PSL;assertion;assertion-based verification;assumption;cover;model checking;property;specification;temporal logic;verification}, 
doi={10.1109/IEEESTD.2010.5446004}, 
month={April},
}
@book{Pree:1995:DPO:189440,
 author = {Pree, Wolfgang},
 title = {Design Patterns for Object-oriented Software Development},
 year = {1995},
 isbn = {0-201-42294-8},
 source = {ACM order no. 704942, member price \$35.75},
 publisher = {ACM Press/Addison-Wesley Publishing Co.},
 address = {New York, NY, USA},
} 
@article{Zhang:2005:FMP:1108906.1108908,
 author = {Zhang, Xinwen and Parisi-Presicce, Francesco and Sandhu, Ravi and Park, Jaehong},
 title = {Formal Model and Policy Specification of Usage Control},
 journal = {ACM Trans. Inf. Syst. Secur.},
 issue_date = {November 2005},
 volume = {8},
 number = {4},
 month = nov,
 year = {2005},
 issn = {1094-9224},
 pages = {351--387},
 numpages = {37},
 url = {http://doi.acm.org/10.1145/1108906.1108908},
 doi = {10.1145/1108906.1108908},
 acmid = {1108908},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Access control, formal specification, security policy, usage control},
} 
@article{Park:2004:UAU:984334.984339,
 author = {Park, Jaehong and Sandhu, Ravi},
 title = {The UCONABC Usage Control Model},
 journal = {ACM Trans. Inf. Syst. Secur.},
 issue_date = {February 2004},
 volume = {7},
 number = {1},
 month = feb,
 year = {2004},
 issn = {1094-9224},
 pages = {128--174},
 numpages = {47},
 url = {http://doi.acm.org/10.1145/984334.984339},
 doi = {10.1145/984334.984339},
 acmid = {984339},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {access control, digital rights management, privacy, trust, usage control},
}
@INPROCEEDINGS{1624011, 
author={A. Barth and A. Datta and J. C. Mitchell and H. Nissenbaum}, 
booktitle={2006 IEEE Symposium on Security and Privacy (S P'06)}, 
title={Privacy and contextual integrity: framework and applications}, 
year={2006}, 
volume={}, 
number={}, 
pages={15 pp.-198}, 
keywords={data integrity;data privacy;temporal logic;COPPA;GLBA;HIPAA;contextual integrity;legislation;personal information;privacy expectations;privacy norms;privacy policy;temporal logic;Access control;Context;Internet;Law;Legal factors;Legislation;Logic;Privacy;Protection;Public policy}, 
doi={10.1109/SP.2006.32}, 
ISSN={1081-6011}, 
month={May},
}
@inproceedings{DeYoung:2010:ELS:1866919.1866930,
 author = {DeYoung, Henry and Garg, Deepak and Jia, Limin and Kaynar, Dilsun and Datta, Anupam},
 title = {Experiences in the Logical Specification of the HIPAA and GLBA Privacy Laws},
 booktitle = {Proceedings of the 9th Annual ACM Workshop on Privacy in the Electronic Society},
 series = {WPES '10},
 year = {2010},
 isbn = {978-1-4503-0096-4},
 location = {Chicago, Illinois, USA},
 pages = {73--82},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1866919.1866930},
 doi = {10.1145/1866919.1866930},
 acmid = {1866930},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {fixed point logic, glba, hipaa, privacy policy specification},
} 
@inproceedings{Hilty:2007:PLD:2393847.2393895,
 author = {Hilty, M. and Pretschner, A. and Basin, D. and Schaefer, C. and Walter, T.},
 title = {A Policy Language for Distributed Usage Control},
 booktitle = {Proceedings of the 12th European Conference on Research in Computer Security},
 series = {ESORICS'07},
 year = {2007},
 isbn = {3-540-74834-2, 978-3-540-74834-2},
 location = {Dresden, Germany},
 pages = {531--546},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=2393847.2393895},
 acmid = {2393895},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 
@Inbook{Barringer2004,
author="Barringer, Howard
and Goldberg, Allen
and Havelund, Klaus
and Sen, Koushik",
editor="Steffen, Bernhard
and Levi, Giorgio",
title="Rule-Based Runtime Verification",
bookTitle="Verification, Model Checking, and Abstract Interpretation: 5th International Conference, VMCAI 2004 Venice, Italy, January 11-13, 2004 Proceedings",
year="2004",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="44--57",
abstract="We present a rule-based framework for defining and implementing finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time logics, interval logics, forms of quantified temporal logics, and so on. Our logic, Eagle, is implemented as a Java library and involves novel techniques for rule definition, manipulation and execution. Monitoring is done on a state-by-state basis, without storing the execution trace.",
isbn="978-3-540-24622-0",
doi="10.1007/978-3-540-24622-0_5",
url="https://doi.org/10.1007/978-3-540-24622-0_5"
}
@article{barringer2010formal,
  title={Formal Analysis of Log Files},
  author={Barringer, Howard and Groce, Alex and Havelund, Klaus and Smith, Margaret H},
  journal={JACIC},
  volume={7},
  number={11},
  pages={365--390},
  year={2010}
}
@inproceedings{Bauer:2009:FPL:1615503.1615511,
 author = {Bauer, Andreas and Gor{\'e}, Rajeev and Tiu, Alwen},
 title = {A First-Order Policy Language for History-Based Transaction Monitoring},
 booktitle = {Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing},
 series = {ICTAC '09},
 year = {2009},
 isbn = {978-3-642-03465-7},
 location = {Kuala Lumpur, Malaysia},
 pages = {96--111},
 numpages = {16},
 url = {http://dx.doi.org/10.1007/978-3-642-03466-4_6},
 doi = {10.1007/978-3-642-03466-4_6},
 acmid = {1615511},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 
@article{Chomicki:1995:ECT:210197.210200,
 author = {Chomicki, Jan},
 title = {Efficient Checking of Temporal Integrity Constraints Using Bounded History Encoding},
 journal = {ACM Trans. Database Syst.},
 issue_date = {June 1995},
 volume = {20},
 number = {2},
 month = jun,
 year = {1995},
 issn = {0362-5915},
 pages = {149--186},
 numpages = {38},
 url = {http://doi.acm.org/10.1145/210197.210200},
 doi = {10.1145/210197.210200},
 acmid = {210200},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {active databases, database integrity, integrity constraints, real-time databases, temporal databases, temporal logic, triggers},
} 
@incollection{Dinesh:2008:CTR:1483018.1483024,
 author = {Dinesh, Nikhil and Joshi, Aravind and Lee, Insup and Sokolsky, Oleg},
 chapter = {Checking Traces for Regulatory Conformance},
 title = {Runtime Verification},
 editor = {Leucker, Martin},
 year = {2008},
 isbn = {978-3-540-89246-5},
 pages = {86--103},
 numpages = {18},
 url = {http://dx.doi.org/10.1007/978-3-540-89247-2_6},
 doi = {10.1007/978-3-540-89247-2_6},
 acmid = {1483024},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 
@inproceedings{Garg:2011:PAO:2046707.2046726,
 author = {Garg, Deepak and Jia, Limin and Datta, Anupam},
 title = {Policy Auditing over Incomplete Logs: Theory, Implementation and Applications},
 booktitle = {Proceedings of the 18th ACM Conference on Computer and Communications Security},
 series = {CCS '11},
 year = {2011},
 isbn = {978-1-4503-0948-6},
 location = {Chicago, Illinois, USA},
 pages = {151--162},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2046707.2046726},
 doi = {10.1145/2046707.2046726},
 acmid = {2046726},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {audit, formal logic, incomplete logs, privacy policy},
} 
@inproceedings{Groce:2010:SSE:1810295.1810314,
 author = {Groce, Alex and Havelund, Klaus and Smith, Margaret},
 title = {From Scripts to Specifications: The Evolution of a Flight Software Testing Effort},
 booktitle = {Proceedings of the 32Nd ACM/IEEE International Conference on Software Engineering - Volume 2},
 series = {ICSE '10},
 year = {2010},
 isbn = {978-1-60558-719-6},
 location = {Cape Town, South Africa},
 pages = {129--138},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1810295.1810314},
 doi = {10.1145/1810295.1810314},
 acmid = {1810314},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Python, development practices, logs, runtime verification, space flight software, temporal logic, test infrastructure, testing},
} 
@ARTICLE{5719595, 
author={S. Halle and R. Villemaire}, 
journal={IEEE Transactions on Services Computing}, 
title={Runtime Enforcement of Web Service Message Contracts with Data}, 
year={2012}, 
volume={5}, 
number={2}, 
pages={192-206}, 
keywords={Java;Web services;XML;temporal logic;Amazon.com;Google;Java applet;LTL-FO+ specification;SOAP Web services;Web service message contracts;XML messages;client-side enforcement architectures;data elements;data parameterization;first-order quantification;linear temporal logic;runtime enforcement;server-side enforcement architectures;stateful behavior;Contracts;Documentation;Google;Monitoring;Runtime;Semantics;Web services;Web services;runtime monitoring;temporal logic.}, 
doi={10.1109/TSC.2011.10}, 
ISSN={1939-1374}, 
month={April},
}
@inproceedings{Maggi:2011:MBC:2040283.2040299,
 author = {Maggi, Fabrizio Maria and Montali, Marco and Westergaard, Michael and Van Der Aalst, Wil M. P.},
 title = {Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata},
 booktitle = {Proceedings of the 9th International Conference on Business Process Management},
 series = {BPM'11},
 year = {2011},
 isbn = {978-3-642-23058-5},
 location = {Clermont-Ferrand, France},
 pages = {132--147},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=2040283.2040299},
 acmid = {2040299},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 keywords = {automata, declare, linear temporal logic, monitoring, runtime verification},
} 
@inproceedings{Roger:2001:LAT:872752.873518,
 author = {Roger, Muriel and Goubault-Larrecq, Jean},
 title = {Log Auditing Through Model-Checking},
 booktitle = {Proceedings of the 14th IEEE Workshop on Computer Security Foundations},
 series = {CSFW '01},
 year = {2001},
 pages = {220--},
 url = {http://dl.acm.org/citation.cfm?id=872752.873518},
 acmid = {873518},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
} 
@ARTICLE{390251, 
author={A. P. Sistla and O. Wolfson}, 
journal={IEEE Transactions on Knowledge and Data Engineering}, 
title={Temporal triggers in active databases}, 
year={1995}, 
volume={7}, 
number={3}, 
pages={471-486}, 
keywords={active databases;formal specification;temporal logic;Future Temporal Logic;Past Temporal Logic;SUN workstations;Sybase;active databases;attribute;temporal triggers;trigger conditions;Application software;Condition monitoring;Data security;Database systems;History;Logic;Sun;Traffic control;Transaction databases;Workstations}, 
doi={10.1109/69.390251}, 
ISSN={1041-4347}, 
month={Jun},
}
@Inbook{Barre2013,
author="Barre, Benjamin
and Klein, Mathieu
and Soucy-Boivin, Maxime
and Ollivier, Pierre-Antoine
and Hall{\'e}, Sylvain",
editor="Qadeer, Shaz
and Tasiran, Serdar",
title="MapReduce for Parallel Trace Validation of LTL Properties",
bookTitle="Runtime Verification: Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="184--198",
abstract="We present an algorithm for the automated verification of Linear Temporal Logic formul{\ae} on event traces using an increasingly popular cloud computing framework called MapReduce. The algorithm can process multiple, arbitrary fragments of the trace in parallel, and compute its final result through a cycle of runs of MapReduce instances. Compared to classical, single-instance solutions, a proof-of-concept implementation shows through experimental evaluation how the algorithm reduces by as much as 90{\%} the number of operations that must be performed linearly, resulting in a commensurate speed gain.",
isbn="978-3-642-35632-2",
doi="10.1007/978-3-642-35632-2_20",
url="https://doi.org/10.1007/978-3-642-35632-2_20"
}
@Inbook{Bianculli2014,
author="Bianculli, Domenico
and Ghezzi, Carlo
and Krsti{\'{c}}, Sr{\dj}an",
editor="Giannakopoulou, Dimitra
and Sala{\"u}n, Gwen",
title="Trace Checking of Metric Temporal Logic with Aggregating Modalities Using MapReduce",
bookTitle="Software Engineering and Formal Methods: 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014. Proceedings",
year="2014",
publisher="Springer International Publishing",
address="Cham",
pages="144--158",
abstract="Modern complex software systems produce a large amount of execution data, often stored in logs. These logs can be analyzed using trace checking techniques to check whether the system complies with its requirements specifications. Often these specifications express quantitative properties of the system, which include timing constraints as well as higher-level constraints on the occurrences of significant events, expressed using aggregate operators.",
isbn="978-3-319-10431-7",
doi="10.1007/978-3-319-10431-7_11",
url="https://doi.org/10.1007/978-3-319-10431-7_11"
}
@Article{Basin2016,
author="Basin, David
and Caronni, Germano
and Ereth, Sarah
and Harvan, Mat{\'u}{\v{s}}
and Klaedtke, Felix
and Mantel, Heiko",
title="Scalable offline monitoring of temporal specifications",
journal="Formal Methods in System Design",
year="2016",
month="Oct",
day="01",
volume="49",
number="1",
pages="75--108",
abstract="We propose an approach to monitoring IT systems offline where system actions are logged in a distributed file system and subsequently checked for compliance against policies formulated in an expressive temporal logic. The novelty of our approach is that monitoring is parallelized so that it scales to large logs. Our technical contributions comprise a formal framework for slicing logs, an algorithmic realization based on MapReduce, and a high-performance implementation. We evaluate our approach analytically and experimentally, proving the soundness and completeness of our slicing techniques and demonstrating its practical feasibility and efficiency on real-world logs with 400 GB of relevant data.",
issn="1572-8102",
doi="10.1007/s10703-016-0242-y",
url="https://doi.org/10.1007/s10703-016-0242-y"
}
